home *** CD-ROM | disk | FTP | other *** search
Text File | 1995-05-30 | 284 b | 9 lines | [TEXT/MPS ] |
-
- # whitespace -- noweb filter to make multiple whitespace
- # characters equivalent to a single space, so that
- # << Hello World>>, <<Hello World>>,
- # and <<Hello World >> all refer to the chunk
- # <<Hello World>>
-
- sed -e '/^@use /s/[ \t][ \t]*/ /g' -e '/^@defn /s/[ \t][ \t]*/ /g'
-